FDL - Step of Proof: nat_ind

Step of Proof: nat_ind_a

9,38

Inference at * 1 3
Iof proof for Lemma nat ind a:

1. P :

{k}
2. P(0)
3.

. P(i - 1)

P(i)
4. i :

5. 0 < i
6. ((i - 1)

0 )

P(i - 1)
7. i

P(i)

by ((((BHyp 3)

CollapseTHENM (BHyp 6))

)

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat

C2:n),(first_nat 3:n)) (first_tok :t) inil_term)))

Definitions False, A, A B, t T, i j , P Q, , x:A. B(x)